tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
TWOTO(s(x1)) → P(s(x1))
TOWER(s(x1)) → P(s(tower(p(s(p(s(x1)))))))
TWICE(s(x1)) → P(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))
TWICE(s(x1)) → P(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
TOWER(s(x1)) → P(s(p(s(x1))))
TOWER(0(x1)) → P(s(p(s(x1))))
TWOTO(s(x1)) → P(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))
TWOTO(s(x1)) → P(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))
TWOTO(s(x1)) → P(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))
TOWER(s(x1)) → P(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
TWOTO(s(x1)) → TWOTO(p(s(p(s(x1)))))
TWOTO(s(x1)) → P(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))
TWOTO(s(x1)) → P(s(s(s(twoto(p(s(p(s(x1)))))))))
TWOTO(s(x1)) → P(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
TOWER(s(x1)) → TOWER(p(s(p(s(x1)))))
TWOTO(s(x1)) → TWICE(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))
TWOTO(s(x1)) → P(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))
P(p(s(x1))) → P(x1)
TOWER(s(x1)) → P(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))
TOWER(0(x1)) → P(s(x1))
TWOTO(s(x1)) → P(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))
TWICE(s(x1)) → P(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))
TOWER(s(x1)) → P(s(x1))
TWOTO(s(x1)) → P(s(p(s(x1))))
TWOTO(s(x1)) → P(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))
TWOTO(s(x1)) → P(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))
TWICE(s(x1)) → P(s(s(s(x1))))
TWOTO(s(x1)) → P(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))
TOWER(s(x1)) → TWOTO(p(s(p(s(tower(p(s(p(s(x1))))))))))
TWOTO(s(x1)) → P(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))
TWOTO(s(x1)) → P(p(s(s(s(twoto(p(s(p(s(x1))))))))))
TWICE(s(x1)) → P(p(p(s(s(s(x1))))))
TWICE(s(x1)) → P(p(s(s(s(x1)))))
TWICE(s(x1)) → TWICE(p(p(p(s(s(s(x1)))))))
TOWER(s(x1)) → P(s(p(s(tower(p(s(p(s(x1)))))))))
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
TWOTO(s(x1)) → P(s(x1))
TOWER(s(x1)) → P(s(tower(p(s(p(s(x1)))))))
TWICE(s(x1)) → P(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))
TWICE(s(x1)) → P(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
TOWER(s(x1)) → P(s(p(s(x1))))
TOWER(0(x1)) → P(s(p(s(x1))))
TWOTO(s(x1)) → P(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))
TWOTO(s(x1)) → P(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))
TWOTO(s(x1)) → P(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))
TOWER(s(x1)) → P(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
TWOTO(s(x1)) → TWOTO(p(s(p(s(x1)))))
TWOTO(s(x1)) → P(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))
TWOTO(s(x1)) → P(s(s(s(twoto(p(s(p(s(x1)))))))))
TWOTO(s(x1)) → P(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
TOWER(s(x1)) → TOWER(p(s(p(s(x1)))))
TWOTO(s(x1)) → TWICE(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))
TWOTO(s(x1)) → P(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))
P(p(s(x1))) → P(x1)
TOWER(s(x1)) → P(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))
TOWER(0(x1)) → P(s(x1))
TWOTO(s(x1)) → P(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))
TWICE(s(x1)) → P(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))
TOWER(s(x1)) → P(s(x1))
TWOTO(s(x1)) → P(s(p(s(x1))))
TWOTO(s(x1)) → P(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))
TWOTO(s(x1)) → P(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))
TWICE(s(x1)) → P(s(s(s(x1))))
TWOTO(s(x1)) → P(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))
TOWER(s(x1)) → TWOTO(p(s(p(s(tower(p(s(p(s(x1))))))))))
TWOTO(s(x1)) → P(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))
TWOTO(s(x1)) → P(p(s(s(s(twoto(p(s(p(s(x1))))))))))
TWICE(s(x1)) → P(p(p(s(s(s(x1))))))
TWICE(s(x1)) → P(p(s(s(s(x1)))))
TWICE(s(x1)) → TWICE(p(p(p(s(s(s(x1)))))))
TOWER(s(x1)) → P(s(p(s(tower(p(s(p(s(x1)))))))))
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
P(p(s(x1))) → P(x1)
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(p(s(x1))) → P(x1)
The value of delta used in the strict ordering is 1/32.
POL(P(x1)) = (1/2)x_1
POL(p(x1)) = (1/4)x_1
POL(s(x1)) = 1/4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
TWICE(s(x1)) → TWICE(p(p(p(s(s(s(x1)))))))
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TWICE(s(x1)) → TWICE(p(p(p(s(s(s(x1)))))))
The value of delta used in the strict ordering is 2.
POL(s(x1)) = 4 + (2)x_1
POL(p(x1)) = (1/2)x_1
POL(0(x1)) = 0
POL(TWICE(x1)) = (4)x_1
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
TWOTO(s(x1)) → TWOTO(p(s(p(s(x1)))))
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TWOTO(s(x1)) → TWOTO(p(s(p(s(x1)))))
The value of delta used in the strict ordering is 1/32.
POL(s(x1)) = 1/4 + (4)x_1
POL(p(x1)) = (1/4)x_1
POL(TWOTO(x1)) = (1/4)x_1
p(s(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
TOWER(s(x1)) → TOWER(p(s(p(s(x1)))))
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOWER(s(x1)) → TOWER(p(s(p(s(x1)))))
The value of delta used in the strict ordering is 1.
POL(TOWER(x1)) = (2)x_1
POL(s(x1)) = 4 + (4)x_1
POL(p(x1)) = 3/4 + (1/4)x_1
p(s(x1)) → x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
tower(0(x1)) → s(0(p(s(p(s(x1))))))
tower(s(x1)) → p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1))))))))))))))
twoto(0(x1)) → s(0(x1))
twoto(s(x1)) → p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))))
twice(0(x1)) → 0(x1)
twice(s(x1)) → p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))))
p(p(s(x1))) → p(x1)
p(s(x1)) → x1
p(0(x1)) → 0(s(s(s(s(s(s(s(s(x1)))))))))